\begin{tabbing}
(\=Fold `p{-}fun{-}exp` 0) \+
\\[0ex]CollapseTHEN ((RWO "p{-}compose{-}associative$<$" 0) 
\\[0ex]CollapseTHEN ((
\-\\[0ex]A\=uto$\cdot$) \+
\\[0ex]CollapseTHEN ((EqCD) 
\\[0ex]CollapseTHEN ((Auto$\cdot$) 
\\[0ex]CollapseTHEN ((if ((0
\-\\[0ex]) = 0) then BackThruSomeHyp else BHyp (0) )$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\end{tabbing}